i, j:. (i  j)  upto(i)  upto(j) 

latex

Definitions	t  T, s = t, x:AB(x), x:A. B(x), {i..j}, as @ bs, type List, , , A  B, s ~ t, a < b, #$n, Type, x:A  B(x), P & Q, i  j < k, , P  Q, False, A, {x:A| B(x)} , S  T, -n, Void, A List, x:A. B(x), |g|, l1  l2, n - m, upto(n), n+m, x.A(x), map(f;as)
Lemmas	iseg wf, upto decomp, map wf, nat wf, upto wf, member wf, le wf, int seg wf, append wf